package ch.epfl.lara.matcheck.verify.transform;

import ch.epfl.lara.matcheck.ast._
import ch.epfl.lara.matcheck.util.FreshName

object Tree2VTree extends PropositionalFormulaMaker {
  
  
  def apply(program: Program): VProgram =  {
    val Program(constr,extr,objs,klasses) = program
    val top_constr = constr match {
      case None => extr
      case Some(f1) => extr match {
        case None => constr
        case Some(f2) => Some(And(f1,f2))
      }
    }
      VProgram(top_constr,
               objs.map(convert(_)) ::: klasses.map(convert(_))
              ).setPos(program.pos)
  }
  
  
  
  
  private def convert(top: TopDecl): VContainer = {
    val (inv,methods) = top match { 
      case ClassDef(_,_,_,_,_,inv,methods) => (inv,methods)
      case ObjectDef(_,inv,methods) => (inv,methods)
    }
    VContainer(inv,methods.map(convert(_)))
  }
  
  
  
  
  
  private def convert(method: MethodDef): VMethodDef = {
    val MethodDef(_,params,_,ppc,body) = method
    VMethodDef(conjunction(params.map(p=>In(Element(p.name.getName),Set(p.tpe.toString)))),
               ppc,
               convert(body)).setPos(method.pos)
  }
  
  
  
  
  
  
  private def convert(body: Expr): VExpr = body match {
    case If(cond,then,elze) => 
      val (lhs,_) = TreeExpr2Formula(cond)
      VIf((lhs,Tru),convert(then),convert(elze)).setPos(body.pos)
    case Match(scrutinee,tpe,cases) =>
      val (lhs_f,fresh) = TreeExpr2Formula(scrutinee)
      val tpeSet = TreeExpr2Formula(tpe)
      VMatch(And(lhs_f,In(Element(fresh),tpeSet)),cases.map(convert(fresh,_))).setPos(body.pos)
    case _ => VSimpleExpr.setPos(body.pos)
  }

  
  
  
  private def convert(scrutinee: String, kase: CaseDef): VCaseDef = {
    val CaseDef(pos,pattern,guard,body) = kase
    val imply @ Imply(lhs,rhs) = Pattern2Formula(scrutinee,pattern)
    val case_formula = guard match {
      case None => imply
      case Some(guard) =>
        val (guard_lhs,fresh) = TreeExpr2Formula(guard)
        Imply(And(lhs,guard_lhs),And(rhs,Element(fresh)))
    }
    VCaseDef(pos,case_formula,convert(body))
  }
 
  
}



